The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Finding tractable methods for program reasoning remains a major research challenge. Here we address this challenge using an integrated approach to tackle a niche program reasoning application. The application is proving exception freedom, i.e. proving that a program is free from run-time exceptions. Exception freedom proofs are a significant task in the development of high integrity software, such...
Recent work on combining CSP and B has provided ways of describing systems comprised of components described in both B (to express requirements on state) and CSP (to express interactive and controller behaviour). This approach is driven by the desire to exploit existing tool support for both CSP and B, and by the need for compositional proof techniques. This paper is concerned with the theory underpinning...
This paper proposes an algorithm for abstracting infinite state CSPZ—formal combination of CSP (behavioural part) and Z (data part)—processes, with the aim of model checking. Differently from previous work, where CSPZ process abstraction is achieved by investigating only its data part, the current approach abstracts by exploring the whole CSP...
We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many...
Behaviour Trees is a novel approach for requirements engineering. It advocates a graphical tree notation that is easy to use and to understand. Individual requirements are modelled as single trees which later on are integrated into a model of the system as a whole. We develop a formal semantics for a subset of Behaviour Trees using CSP. This work, on one hand, provides tool support for Behaviour Trees...
The requirements capture of complex systems requires powerful mechanisms for specifying system state, structure and interactive behaviors. Integrated formal specification languages are well suited for presenting more complete and coherent requirement models for complex systems. Given an integrated model, one can project it into multiple views for specialized analysis. Message Sequence Charts (MSCs)...
The integration of UML and formal methods such as B and SMV provides a bridge between graphical specification techniques usable by mainstream software engineers, and precise analysis and verification techniques, essential for the development of high integrity and critical systems. In this paper we define a translation from UML class diagrams into B, which is used to verify the consistency of UML models...
We present an approach to integrating the refinement relation between infinite integer types (used in specification languages) and finite integer types (used in programming languages) into software verification calculi. Since integer types in programming languages have finite ranges, in general they are not a correct data refinement of the mathematical integers usually used in specification languages...
The correctness of design decisions is a very relevant aspect of building any software or hardware system. Emerging techniques tend to include formal methods in the system design flow. Together with older, established techniques, already well known to the present day designer, the combined approach should bring benefits in the form of correctness of the design, increase of reliability, etc, all these...
This paper shows how to translate the problem of deciding trace refinement between two data independent (DI) CSP processes to an unreachability problem in a DI Unity program. We cover here the straightforward but practically useful case when the specification satisfies a normality condition, Norm, meaning that we do not have to worry about hidden or unrecorded data variables. This allows us to transfer...
We describe how CSP-OZ, an integrated formal method combining the process algebra CSP with the specification language Object-Z, can be linked to standard software engineering languages, viz. UML and Java. Our aim is to generate a significant part of the CSP-OZ specification from an initially developed UML model using a UML profile for CSP-OZ, and afterwards transform the formal specification into...
In this paper, we address the problem of expressing object-oriented concepts in terms of Petri nets. This is interesting, first, as a possibility of representing concurrent system specifications written in object-oriented formalisms or languages with Petri nets, and second, as a way of allowing automated verification of the obtained Petri net using existing reachability analysis tools. We start...
We introduce a new specification formalism which we call hiddenCCS; hidden algebra is used to specify local goals as objects, and CCS is used to describe global goal of the synchronizing concurrent objects. We extend the object specification with synchronization elements associated with methods of different objects, and we use a CCS coordinating module to describe the interaction patterns of methods...
Object-Z has a repertoire of operation operators and admits recursively defined operations to permit complex operations to be expressed compositionally via more primitive operation components. Although the operators are rigorously defined in the literature, some of these definitions are intuitively obscure. In this paper we interpret Object-Z class operations as generalised substitutions, thus investing...
We study the expressive power of two modelling formalisms, viz. hybrid automata and μCRLt. The automaton based language of hybrid automata is a popular formalism that is used for describing and analysing the behaviours of hybrid systems. The process algebraic language μCRLt is designed for specifying real-time and data-dependent systems and to reason...
Computer aided hardware/software partitioning is one of the key challenges in hardware/software co-design. This paper describes a new approach to hardware/software partitioning for synchronous communication model. We transform the partitioning into a reachability problem of timed automata. By means of an optimal reachability algorithm, an optimal solution can be obtained in terms of limited resources...
In order to reconcile the state of the art and the state of the practice in software engineering, immediate goals aim to use formal methods in ways that are minimally disruptive to professional practice. In this pursuit formal methods should be adapted to flexible lifecycle structures, getting over more traditional approaches. In the field of real-time design, SCTL/MUS-T methodology proposes a software...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.